package extensionTools.smvCreator;

import java.util.ArrayList;


import extensionTools.smvCreator.Exceptions.RulesUtilsException;

/**
 * This class's purpose is to give tools to create SMV files according to the SMV syntax
 * @author oshrit & lital & dani
 *
 */
public class SmvOp {
        
        static public String not(String param)
        {
            return "!("+param+")";
        }
        
        static public String and(String param1, String param2)
        {
        	if (param1 == null || param2 == null)
        	{
        		return null;
        	}
        	if (param1 == "")
        	{
        		return param2;
        	}
        	if (param2 == "")
        	{
        		return param1;
        	}
            return param1+" & "+param2;
        }
        /*
         * And function with unbound number of params
         */
        static public String and(String... params) {
                
                String andConcat = "" ;
                boolean inStart = false;
                for (String param : params ) {
                        if (inStart == false)
                        {
                                andConcat+=param;
                                inStart = true;
                        }
                        else
                        {   
                        	if (param != "")
                        	{
                        		andConcat+=" & " + param;
                        	}
                        }
                }
                return andConcat;
        }

        static public String or(String param1, String param2)
        {
            return "( " + param1 + " ) " + " | " + " ( " + param2 + " ) ";
        }
        
        static public String defVar (String param, String type)
        {
            param=setFirstCharToLowerCase(param);
            return param+" : "+type + ";\n";
        }
        
        static public String init (String param, String val)
        {
            param=setFirstCharToLowerCase(param);
            
            return "\tinit(" + param +"):=" + val + ";\n";  
        }
        
        static public String next (String param, String nextVal)
        {
            param=setFirstCharToLowerCase(param);
            return "\tnext(" + param +") :=" + nextVal + ";\n";      
        }
        
        static public String assignToParam (String param, String assignVal)
        {
            param=setFirstCharToLowerCase(param);
            return "\t"+param+" := " + assignVal + ";\n";
        }
                
        /**
         * @param rules A list of case rules
         * @return a case structure for the "next" assignment
         */
        static public String createCase (String[] rules){
            if (rules == null || rules.length <=0){
                    return null;
            }
            String caseStr = " case";
            for (String curRule : rules) {
            		if (curRule != null || curRule != "")
                    caseStr+="\n\t\t\t"+ curRule;
            } 
            return caseStr + "\n\t\t\tesac";
        }
        /**
         * @param unbound list of of rules for the case rule
         * @return a case structure for the "next" assignment
         */
        static public String createCaseS (String... rules){
            String caseStr = " case";
            for (String curRule : rules) {
                    caseStr+="\n\t\t\t"+ curRule;
            } 
            return caseStr + "\n\t\t\tesac";
    }
        /**
         * This function combines the different parts of the Smv code
         * @param initParams
         * @param declaration
         * @param body
         * @return A combined string
         */
        static public String smvTemplate (String initParams, String declaration, String body)
        {
            String temp=  "MODULE main\n"+ "VAR\n" + initParams + "\nASSIGN\n" + declaration;
            //if there are no things to check, we won't be adding the "TRANS" chapter
            if (body != null && !body.equals("")){  
                             temp+= "\nTRANS\n" + body;
            }
            return temp;
        }
        
        /**
         * This function turns params and result into a valid Smv case line
         * @param arg
         * @param res
         * @return
         * @throws RulesUtilsException - when null parameters were sent
         */
        static public String createCaseLine(String arg,String res) throws RulesUtilsException {           
            if (arg == null || res == null)
            {
            	throw new RulesUtilsException("SmvOp: got null parameters in createCaseLine");
            }
            String caseLine = arg + " : " + res + ";";
            return caseLine;
        }
        
        /**
         * This function sets a variable to be legal in SMV syntax
         * @param stringToLower
         * @return the variable in legal SMV syntax
         */
        static String setFirstCharToLowerCase(String stringToLower)
        {
        	if(stringToLower == "") return stringToLower;
            //String firstLetter = stringToLower.substring(0,1).toLowerCase();
            return stringToLower.substring(0,1).toLowerCase().concat(stringToLower.substring(1));
        }
        
        
        
        /**
         * 
         * @param term
         * @return result string for termination lottery
         */
        static public String prepareTerminationRes(int term) 
        {
            String res = "{0";
            for (int j = 1; j < term; j++) 
            {
                    res+= ","+j;
            }
            res += "}";
            
            return res;
        }

        /**
         * This function create for a list like this (item_1,item_2,...item_n)
         * a list like this {item_1,item_2,...item_n} usually used for a SMV enumeration
         * @param itemList
         * @return String like this {item_1,item_2,...item_n}
         * @throws RulesUtilsException - when null parameters were sent
         */
        public static String prepareBrackets(ArrayList<String> itemList) throws RulesUtilsException {
                
                if (itemList == null || itemList.size() == 0)
                {
                        throw new RulesUtilsException("SmvOp: Null parameters sent to smvOp.prepareBrackets");
                }
                String res = "{";
                
                for (String items: itemList)
                {
                        res+=items+",";
                }
                res = res.substring(0, res.lastIndexOf(","));
                res+="}";
        return res;
        }
        
}
